Metamath Blueprint : AKS (PRIMES is in P)
Theorem
aks61c4
Status:
Draft
Reference:
Claim 4 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf